es:ES, e1:E, e2:{e:E| loc(e) = loc(e1)  Id }. e[e1,e2).False  e2  e1  

latex

Definitions	False, e  e' , t  T, x:A. B(x), (e <loc e'), Prop, P  Q, E, e[e1,e2).P(e), P  Q, P  Q, b, A, loc(e), Id, x. t(x), P & Q, P  Q, ES
Lemmas	es-le-loc, es-locl-iff, es-le-trans2, es-le-not-locl, es-le-self, event system wf, alle-between1 wf, false wf, Id wf, es-loc wf, es-loc-pred, es-E wf, es-le wf, es-locl wf